Inference at * 1 1 
Iof proof for Lemma bool-to-dcdr wf:

.....assertion..... NILNIL

1. A : Type
2. f : A
3. A
  {f}  (x:A. Dec(f(x) = tt)) 

latex

 by (Unfold `bool-to-dcdr` 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions

{f}